/*
 * Alloy Analyzer 4 -- Copyright (c) 2006-2008, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package edu.ut.ece382c.valloy.ast;

import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.JoinableList;
import static edu.ut.ece382c.valloy.ast.Type.EMPTY;

/**
 * Immutable; represents an expression of the form (x OP y).
 *
 * <p> <b>Invariant:</b>  type!=EMPTY => (this.mult!=1)
 * <p> <b>Invariant:</b>  type!=EMPTY => (this.mult==2 => this.op is one of the 17 arrow operators)
 * <p> <b>Invariant:</b>  type!=EMPTY => (left.mult!=1)
 * <p> <b>Invariant:</b>  type!=EMPTY => (left.mult==2 => this.op is one of the 17 arrow operators)
 * <p> <b>Invariant:</b>  type!=EMPTY => (right.mult==1 => this.op==IN)
 * <p> <b>Invariant:</b>  type!=EMPTY => (right.mult==2 => (this.op==IN || this.op is one of the 17 arrow operators))
 */

public final class ExprBinary extends Expr {

    /** The binary operator. */
    public final Op op;

    /** The left-hand-side expression. */
    public final Expr left;

    /** The right-hand-side expression. */
    public final Expr right;

    /** Caches the span() result. */
    private Pos span = null;

    //============================================================================================================//

    /** Constructs a new ExprBinary node. */
    private ExprBinary(Pos pos, Pos closingBracket, Op op, Expr left, Expr right, Type type, JoinableList<Err> errors) {
        super(pos,
            closingBracket,
            left.ambiguous || right.ambiguous,
            type,
            (op.isArrow && (left.mult==2 || right.mult==2 || op!=Op.ARROW))?2:0,
            left.weight + right.weight,
            errors);
        this.op=op;
        this.left=left;
        this.right=right;
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public Pos span() {
        Pos p=span;
        if (p==null) span = (p = pos.merge(closingBracket).merge(right.span()).merge(left.span()));
        return p;
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public void toString(StringBuilder out, int indent, boolean newline) {
    	for(int i=0; i<indent && newline; i++) { out.append(' '); }
        
    	if (op==Op.ISSEQ_ARROW_LONE) 
            out.append("seq "); 
    	else { 
           	left.toString(out,indent, false); 
            out.append(' ').append(op).append(' '); 
    	}
    	right.toString(out, indent, false);
    }

    //============================================================================================================//

    /** This class contains all possible binary operators. */
    public static enum Op {
        /** -&gt;           */  ARROW("->",true),
        /** -&gt;some       */  ANY_ARROW_SOME("->some",true),
        /** -&gt;one        */  ANY_ARROW_ONE("->one",true),
        /** -&gt;lone       */  ANY_ARROW_LONE("->lone",true),
        /** some-&gt;       */  SOME_ARROW_ANY("some->",true),
        /** some-&gt;some   */  SOME_ARROW_SOME("some->some",true),
        /** some-&gt;one    */  SOME_ARROW_ONE("some->one",true),
        /** some-&gt;lone   */  SOME_ARROW_LONE("some->lone",true),
        /** one-&gt;        */  ONE_ARROW_ANY("one->",true),
        /** one-&gt;some    */  ONE_ARROW_SOME("one->some",true),
        /** one-&gt;one     */  ONE_ARROW_ONE("one->one",true),
        /** one-&gt;lone    */  ONE_ARROW_LONE("one->lone",true),
        /** lone-&gt;       */  LONE_ARROW_ANY("lone->",true),
        /** lone-&gt;some   */  LONE_ARROW_SOME("lone->some",true),
        /** lone-&gt;one    */  LONE_ARROW_ONE("lone->one",true),
        /** lone-&gt;lone   */  LONE_ARROW_LONE("lone->lone",true),
        /** isSeq-&gt;lone  */  ISSEQ_ARROW_LONE("isSeq->lone",true),
        /** .               */  JOIN(".",false),
        /** &lt;:           */  DOMAIN("<:",false),
        /** :&gt;           */  RANGE(":>",false),
        /** &amp;           */  INTERSECT("&",false),
        /** ++              */  PLUSPLUS("++",false),
        /** +               */  PLUS("+",false),
        /** -               */  MINUS("-",false),
        /** add             */  ADD("fun/add",false),
        /** subtract        */  SUB("fun/sub",false),
        /** multiply        */  MUL("fun/mul",false),
        /** divide          */  DIV("fun/div",false),
        /** remainder       */  REM("fun/rem",false),
        /** =               */  EQUALS("=",false),
        /** &lt;            */  LT("<",false),
        /** =&lt;           */  LTE("<=",false),
        /** &gt;            */  GT(">",false),
        /** &gt;=           */  GTE(">=",false),
        /** &lt;&lt;        */  SHL("<<",false),
        /** &gt;&gt;        */  SHA(">>",false),
        /** &gt;&gt;&gt;    */  SHR(">>>",false),
        /** in              */  IN("in",false),
        /** &amp;&amp;      */  AND("&&",false),
        /** ||              */  OR("||",false),
        /** &lt;=&gt;       */  IFF("<=>",false);

        /**
         * The constructor.
         * @param label - the label (for printing debugging messages)
         * @param isArrow - true if this operator is one of the 17 arrow operators
         */
        private Op(String label, boolean isArrow) {
            this.label=label;
            this.isArrow=isArrow;
        }

        /** The human readable label for this operator. */
        private final String label;

        /**
         * True if and only if this operator is the Cartesian product "->", a "seq" multiplicity,
         * or is a multiplicity arrow of the form "?->?".
         */
        public final boolean isArrow;

        /**
         * Constructs a new ExprBinary node.
         * @param pos - the original position in the source file (can be null if unknown)
         * @param left - the left hand side expression
         * @param right - the right hand side expression
         */
        public final Expr make(Pos pos, Pos closingBracket, Expr left, Expr right) {
        	
        	switch(this) {
        		case AND: return ExprList.makeAND(left, right);
        		case OR: return ExprList.makeOR(left, right);
        	}
        	
        	return new ExprBinary(pos, closingBracket, this, left, right, EMPTY, null);
        }

        /** Returns the human readable label for this operator. */
        @Override public final String toString() { return label; }

    }

    //============================================================================================================//


    //============================================================================================================//

    /** {@inheritDoc} */
    public int getDepth() {
        int a=left.getDepth(), b=right.getDepth();
        if (a>=b) return 1+a; else return 1+b;
    }

    /** {@inheritDoc} */
    @Override final<T> T accept(VisitReturn<T> visitor) throws Err { return visitor.visit(this); }
}
